the_w:world{i:l}. fair-fifo{i:l}(the_w)  Prop{i'} 

latex

Definitions

#$n, a(i;t), msg(a), t  T, ||as||, w.M, Msg(M), P  Q, False, A, AB, ij, , {x:A| B(x) }, , Msg, x:AB(x), x:A. B(x), World, Id, IdLnk, isrcv(l;a), b, destination(l), <a,b>, s = t, n+m, a<b, Void, w-atom-constraint(w), w-machine-constraint(w), x:AB(x), P & Q, type List, nil, queue(l;t), Type, left+right, P  Q, x:A. B(x), hd(l), A & B, Prop, mlnk(m), source(l), S  T, m(i;t), s(i;t).x, vartype(i;x), isnull(a), onlnk(l;mss), FairFifo, {T}, kind(a), lnk(k)

Lemmas

assert-w-isrcvl, w-msg wf, not wf, w-onlnk wf, w-isnull wf, w-vartype wf, w-s wf, w-m wf, Msg wf, lsrc wf, mlnk wf, w-M wf, ge wf, length wf1, hd wf, ldst wf, w-queue wf, w-Msg wf, w-machine-constraint wf, w-atom-constraint wf, le wf, assert wf, w-isrcvl wf, w-a wf, IdLnk wf, nat wf, Id wf, world wf